Library waw_conjugate
Require Import PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition waw_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h p q r x y z := p*(x^2×q^2×r^2 + 2×p^2×(r×y - q×z)^2 - p×q×r^2×x×y - p×q^2×r×x×z) in
cTriple (h p q r u v w) (h q r p v w u) (h r p q w u v)
end.
Lemma X5_is_waw_conjugate_of_X2_X141 :
eq_points X_5 (waw_conjugate X_2 X_141).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition waw_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h p q r x y z := p*(x^2×q^2×r^2 + 2×p^2×(r×y - q×z)^2 - p×q×r^2×x×y - p×q^2×r×x×z) in
cTriple (h p q r u v w) (h q r p v w u) (h r p q w u v)
end.
Lemma X5_is_waw_conjugate_of_X2_X141 :
eq_points X_5 (waw_conjugate X_2 X_141).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.